0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 189 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 11 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 0 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
reverseB_in_ga([], []) → reverseB_out_ga([], [])
reverseB_in_ga(.(T24, []), .(T24, [])) → reverseB_out_ga(.(T24, []), .(T24, []))
reverseB_in_ga(.(T51, .(T50, [])), .(T50, .(T51, []))) → reverseB_out_ga(.(T51, .(T50, [])), .(T50, .(T51, [])))
reverseB_in_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, [])))) → reverseB_out_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, []))))
reverseB_in_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, []))))) → reverseB_out_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, [])))))
reverseB_in_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, [])))))) → reverseB_out_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, []))))))
reverseB_in_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, []))))))) → reverseB_out_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, [])))))))
reverseB_in_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, [])))))))) → reverseB_out_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, []))))))))
reverseB_in_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, reverseA_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
reverseA_in_ggga([], T397, T398, .(T397, T398)) → reverseA_out_ggga([], T397, T398, .(T397, T398))
reverseA_in_ggga(.(T409, T410), T411, T412, T414) → U1_ggga(T409, T410, T411, T412, T414, reverseA_in_ggga(T410, T409, .(T411, T412), T414))
U1_ggga(T409, T410, T411, T412, T414, reverseA_out_ggga(T410, T409, .(T411, T412), T414)) → reverseA_out_ggga(.(T409, T410), T411, T412, T414)
U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, reverseA_out_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)) → reverseB_out_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
reverseB_in_ga([], []) → reverseB_out_ga([], [])
reverseB_in_ga(.(T24, []), .(T24, [])) → reverseB_out_ga(.(T24, []), .(T24, []))
reverseB_in_ga(.(T51, .(T50, [])), .(T50, .(T51, []))) → reverseB_out_ga(.(T51, .(T50, [])), .(T50, .(T51, [])))
reverseB_in_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, [])))) → reverseB_out_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, []))))
reverseB_in_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, []))))) → reverseB_out_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, [])))))
reverseB_in_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, [])))))) → reverseB_out_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, []))))))
reverseB_in_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, []))))))) → reverseB_out_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, [])))))))
reverseB_in_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, [])))))))) → reverseB_out_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, []))))))))
reverseB_in_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, reverseA_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
reverseA_in_ggga([], T397, T398, .(T397, T398)) → reverseA_out_ggga([], T397, T398, .(T397, T398))
reverseA_in_ggga(.(T409, T410), T411, T412, T414) → U1_ggga(T409, T410, T411, T412, T414, reverseA_in_ggga(T410, T409, .(T411, T412), T414))
U1_ggga(T409, T410, T411, T412, T414, reverseA_out_ggga(T410, T409, .(T411, T412), T414)) → reverseA_out_ggga(.(T409, T410), T411, T412, T414)
U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, reverseA_out_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)) → reverseB_out_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367)
REVERSEB_IN_GA(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U2_GA(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, reverseA_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
REVERSEB_IN_GA(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → REVERSEA_IN_GGGA(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)
REVERSEA_IN_GGGA(.(T409, T410), T411, T412, T414) → U1_GGGA(T409, T410, T411, T412, T414, reverseA_in_ggga(T410, T409, .(T411, T412), T414))
REVERSEA_IN_GGGA(.(T409, T410), T411, T412, T414) → REVERSEA_IN_GGGA(T410, T409, .(T411, T412), T414)
reverseB_in_ga([], []) → reverseB_out_ga([], [])
reverseB_in_ga(.(T24, []), .(T24, [])) → reverseB_out_ga(.(T24, []), .(T24, []))
reverseB_in_ga(.(T51, .(T50, [])), .(T50, .(T51, []))) → reverseB_out_ga(.(T51, .(T50, [])), .(T50, .(T51, [])))
reverseB_in_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, [])))) → reverseB_out_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, []))))
reverseB_in_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, []))))) → reverseB_out_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, [])))))
reverseB_in_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, [])))))) → reverseB_out_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, []))))))
reverseB_in_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, []))))))) → reverseB_out_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, [])))))))
reverseB_in_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, [])))))))) → reverseB_out_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, []))))))))
reverseB_in_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, reverseA_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
reverseA_in_ggga([], T397, T398, .(T397, T398)) → reverseA_out_ggga([], T397, T398, .(T397, T398))
reverseA_in_ggga(.(T409, T410), T411, T412, T414) → U1_ggga(T409, T410, T411, T412, T414, reverseA_in_ggga(T410, T409, .(T411, T412), T414))
U1_ggga(T409, T410, T411, T412, T414, reverseA_out_ggga(T410, T409, .(T411, T412), T414)) → reverseA_out_ggga(.(T409, T410), T411, T412, T414)
U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, reverseA_out_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)) → reverseB_out_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367)
REVERSEB_IN_GA(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U2_GA(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, reverseA_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
REVERSEB_IN_GA(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → REVERSEA_IN_GGGA(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)
REVERSEA_IN_GGGA(.(T409, T410), T411, T412, T414) → U1_GGGA(T409, T410, T411, T412, T414, reverseA_in_ggga(T410, T409, .(T411, T412), T414))
REVERSEA_IN_GGGA(.(T409, T410), T411, T412, T414) → REVERSEA_IN_GGGA(T410, T409, .(T411, T412), T414)
reverseB_in_ga([], []) → reverseB_out_ga([], [])
reverseB_in_ga(.(T24, []), .(T24, [])) → reverseB_out_ga(.(T24, []), .(T24, []))
reverseB_in_ga(.(T51, .(T50, [])), .(T50, .(T51, []))) → reverseB_out_ga(.(T51, .(T50, [])), .(T50, .(T51, [])))
reverseB_in_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, [])))) → reverseB_out_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, []))))
reverseB_in_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, []))))) → reverseB_out_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, [])))))
reverseB_in_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, [])))))) → reverseB_out_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, []))))))
reverseB_in_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, []))))))) → reverseB_out_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, [])))))))
reverseB_in_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, [])))))))) → reverseB_out_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, []))))))))
reverseB_in_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, reverseA_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
reverseA_in_ggga([], T397, T398, .(T397, T398)) → reverseA_out_ggga([], T397, T398, .(T397, T398))
reverseA_in_ggga(.(T409, T410), T411, T412, T414) → U1_ggga(T409, T410, T411, T412, T414, reverseA_in_ggga(T410, T409, .(T411, T412), T414))
U1_ggga(T409, T410, T411, T412, T414, reverseA_out_ggga(T410, T409, .(T411, T412), T414)) → reverseA_out_ggga(.(T409, T410), T411, T412, T414)
U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, reverseA_out_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)) → reverseB_out_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367)
REVERSEA_IN_GGGA(.(T409, T410), T411, T412, T414) → REVERSEA_IN_GGGA(T410, T409, .(T411, T412), T414)
reverseB_in_ga([], []) → reverseB_out_ga([], [])
reverseB_in_ga(.(T24, []), .(T24, [])) → reverseB_out_ga(.(T24, []), .(T24, []))
reverseB_in_ga(.(T51, .(T50, [])), .(T50, .(T51, []))) → reverseB_out_ga(.(T51, .(T50, [])), .(T50, .(T51, [])))
reverseB_in_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, [])))) → reverseB_out_ga(.(T88, .(T87, .(T86, []))), .(T86, .(T87, .(T88, []))))
reverseB_in_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, []))))) → reverseB_out_ga(.(T135, .(T134, .(T133, .(T132, [])))), .(T132, .(T133, .(T134, .(T135, [])))))
reverseB_in_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, [])))))) → reverseB_out_ga(.(T192, .(T191, .(T190, .(T189, .(T188, []))))), .(T188, .(T189, .(T190, .(T191, .(T192, []))))))
reverseB_in_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, []))))))) → reverseB_out_ga(.(T259, .(T258, .(T257, .(T256, .(T255, .(T254, [])))))), .(T254, .(T255, .(T256, .(T257, .(T258, .(T259, [])))))))
reverseB_in_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, [])))))))) → reverseB_out_ga(.(T336, .(T335, .(T334, .(T333, .(T332, .(T331, .(T330, []))))))), .(T330, .(T331, .(T332, .(T333, .(T334, .(T335, .(T336, []))))))))
reverseB_in_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367) → U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, reverseA_in_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367))
reverseA_in_ggga([], T397, T398, .(T397, T398)) → reverseA_out_ggga([], T397, T398, .(T397, T398))
reverseA_in_ggga(.(T409, T410), T411, T412, T414) → U1_ggga(T409, T410, T411, T412, T414, reverseA_in_ggga(T410, T409, .(T411, T412), T414))
U1_ggga(T409, T410, T411, T412, T414, reverseA_out_ggga(T410, T409, .(T411, T412), T414)) → reverseA_out_ggga(.(T409, T410), T411, T412, T414)
U2_ga(T365, T364, T363, T362, T361, T360, T359, T357, T358, T367, reverseA_out_ggga(T358, T357, .(T359, .(T360, .(T361, .(T362, .(T363, .(T364, .(T365, []))))))), T367)) → reverseB_out_ga(.(T365, .(T364, .(T363, .(T362, .(T361, .(T360, .(T359, .(T357, T358)))))))), T367)
REVERSEA_IN_GGGA(.(T409, T410), T411, T412, T414) → REVERSEA_IN_GGGA(T410, T409, .(T411, T412), T414)
REVERSEA_IN_GGGA(.(T409, T410), T411, T412) → REVERSEA_IN_GGGA(T410, T409, .(T411, T412))
From the DPs we obtained the following set of size-change graphs: